T:Type, m:, L:(T List). (m < ||L||)  (nth_tl(m;L) ~ [L[m] / nth_tl(1+m;L)]) 

latex

Definitions	False, A, A  B, i  j , P  Q, True, ff, i <z j, b, Y, nth_tl(n;as), if b then t else f fi , l[i], , tt, i z j, t  T, T, P  Q, P & Q, P  Q, x:A. B(x), , Unit, ,
Lemmas	ge wf, nat properties, bnot wf, lt int wf, le wf, assert wf, bool wf, le int wf, list decomp, assert of lt int, bnot of le int, true wf, squash wf, eqff to assert, assert of le int, eqtt to assert, iff transitivity, tl wf, length wf1, length tl